{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
  FlexibleContexts, FlexibleInstances, UndecidableInstances,
  ScopedTypeVariables  #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module CnvRel (Idiom, Convert(..)) where

import TypeBasics
import Yoko



import Control.Applicative





instance Convert cnv sum t => Convert cnv (DCsOf a sum) t where
  convert cnv = convert cnv . unDCsOf





type family Idiom cnv :: * -> *
class Applicative (Idiom cnv) => Convert cnv a t where
  convert :: cnv -> a -> Idiom cnv t





instance (Convert cnv a t, Convert cnv b t
         ) => Convert cnv (a :+: b) t where
  convert cnv = foldPlus (convert cnv) (convert cnv)

-- NB only works if there's exactly one matching constructor
instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
          ConvertRs cnv (Rep dc) (Rep dc'),
          DC dc', Range dc' ~ t, DT t
         ) => Convert cnv (N dc) t where
  convert cnv = 
    foldN $ liftA (rejoin . (id :: dc' -> dc') . obj) . convertRs cnv . rep



type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (Equal s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)



-- applies cnv to every Rec in a product; identity on other factors
class Applicative (Idiom cnv) => ConvertRs cnv prod prod' where
  convertRs :: cnv -> prod -> Idiom cnv prod'

instance Convert cnv a b => ConvertRs cnv (Rec a) (Rec b) where
  convertRs cnv (Rec x) = Rec <$> convert cnv x

instance Applicative (Idiom cnv) => ConvertRs cnv (Dep a) (Dep a) where
  convertRs _ = pure
instance Applicative (Idiom cnv) => ConvertRs cnv U       U       where
  convertRs _ = pure

instance (ConvertRs cnv a a', ConvertRs cnv b b'
         ) => ConvertRs cnv (a :*: b) (a' :*: b') where
  convertRs cnv (a :*: b) =
    (:*:) <$> convertRs cnv a <*> convertRs cnv b
